\begin{tabbing}
$\forall$\=${\it es}$:ES, $P_{1}$, $Q_{1}$, $P_{2}$, $Q_{2}$:(E$\rightarrow\mathbb{P}$), ${\it dcd\_P}_{1}$:($e$:E$\rightarrow$Dec($P_{1}$($e$))), $f$:(\{$e$:E$\mid$ $P_{1}$($e$)\} $\rightarrow$\{$e$:E$\mid$ $Q_{1}$($e$)\} ),\+
\\[0ex]$g$:(\{$e$:E$\mid$ $P_{2}$($e$)\} $\rightarrow$\{$e$:E$\mid$ $Q_{2}$($e$)\} ).
\-\\[0ex]($Q_{1}$ $\leftarrow$==$f$== $P_{1}$ \& $Q_{2}$ $\leftarrow$==$g$== $P_{2}$)
\\[0ex]$\Rightarrow$ $\lambda$$e$.($Q_{1}$($e$)) $\vee$ ($Q_{2}$($e$)) $\leftarrow$==[$P_{1}$? $f$ : $g$]== $\lambda$$e$.($P_{1}$($e$)) $\vee$ ($P_{2}$($e$))
\end{tabbing}